l:IdLnk, da:k:Knd fp Type. dt(l;da)  tg:Id fp Type 

latex

Definitions	Knd, t  T, isl(x), , if b t else f fi, x:A. B(x), b, rcv(l,tg), P  Q, , Unit, tag(k), lnk(k), a = b, isrcv(k), x. t(x), compose-fpf(a;b;f), a:A fp B(a), dt(l;da), IdLnk, Id, false, A, b, Prop, P & Q, P  Q, False, True
Lemmas	not functionality wrt iff, assert-eq-lnk, true wf, false wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, bfalse wf, fpf wf, IdLnk wf, compose-fpf wf, isrcv wf, ifthenelse wf, eq lnk wf, lnk wf, tagof wf, unit wf, it wf, rcv wf, Id wf, assert wf, Knd wf